Issue2132.agda:23,8-12
C′ != c of type D
when checking that the expression refl has type C′ ≡ c
